/* Assignment 1 */
/* James Gregory: 3288801        Huy Nguyen: 3430069*/
/* Assume that there are one reader and one writer and counter has 4 bits instead of bytes */

#define NUMBER_OF_BIT 4
#define READERS 1

/*
	Shared Variables
*/
bit shared_counter[2 * NUMBER_OF_BIT];
byte current_val;
byte lo[READERS + 1];
byte hi[READERS + 1];
byte reader_val[READERS + 1];

/*
	Macros
*/
inline increment_locally() {
	d_step {
		byte current_bit = NUMBER_OF_BIT;
		writer_local_counter[current_bit] = (writer_local_counter[current_bit] + 1) % 2;
		writer_local_counter[2*NUMBER_OF_BIT - 1 -current_bit] = writer_local_counter[current_bit];
	
		do
			:: (writer_local_counter[current_bit] == 0);
				if
					:: ((current_bit + 1) < 2*NUMBER_OF_BIT);
						current_bit++;
						writer_local_counter[current_bit] = (writer_local_counter[current_bit] + 1) % 2;
						writer_local_counter[2*NUMBER_OF_BIT - 1 -current_bit] = writer_local_counter[current_bit];
					:: ((current_bit + 1) >= 2*NUMBER_OF_BIT);
						break;
				fi
			:: (writer_local_counter[current_bit] != 0);
				break;
		od
	}
	
}


inline writer_counter_to_int(num) {
	d_step {
		num = 0;
		byte i;
		for(i : 0 .. NUMBER_OF_BIT-1) {
			num = num * 2;
			num = num + writer_local_counter[i];
		}
	}
}

inline counter_to_int() {
    reader_val[_pid] = 0;
    for(i : 0 .. NUMBER_OF_BIT-1) {
        reader_val[_pid] = reader_val[_pid] * 2;
        reader_val[_pid] = reader_val[_pid] + local_counter[i];
    }
}


/*
	Processes
*/

active proctype writer() {
	
	bit writer_local_counter[2 * NUMBER_OF_BIT];
    byte writer_val;
	int j;
	do  :: increment_locally();
           writer_counter_to_int(writer_val);
	       for (j : 1 .. 2*NUMBER_OF_BIT) {
		       shared_counter[2*NUMBER_OF_BIT - j] = writer_local_counter[2*NUMBER_OF_BIT - j];
		   }
           current_val = writer_val;
wf:		   skip;
	od
}

active [READERS] proctype reader() {
	
	bit local_counter[2 * NUMBER_OF_BIT];
	byte i;
	
	do	::
		/* Minimum correct read value */
        lo[_pid] = current_val;
		
		/* Read from shared counter into local copy */
readsc:	for (i : 0 .. (2*NUMBER_OF_BIT-1)) {
			local_counter[i] = shared_counter[i];
		};
		
		/* A maximum correct read value */
		hi[_pid] = current_val;
		/* Attempt to locally deduce a value */
		/* This can be done atomically as it only involves local calculations */
deduce:	d_step {
			bool max = false;
			for (i : 0 .. NUMBER_OF_BIT-1) {
				if
					:: max ->
						local_counter[i] = 1
					:: else ->
						max = (local_counter[i] != local_counter[2*NUMBER_OF_BIT - 1 - i])
				fi
			}
			counter_to_int();
		}
rf:		skip;		
	od
}

ltl read_in_range { [](reader[1]@rf -> (reader_val[1] >= 0 && reader_val[1] <= 15)) }

ltl correct_read_1 { []((writer@wf && reader[1]@rf && (lo[1] < hi[1])) -> (reader_val[1] >= lo[1] && reader_val[1] <= hi[1])) }

ltl correct_read_2 { []((writer@wf && reader[1]@rf && (lo[1] > hi[1])) -> (reader_val[1] < hi[1] || reader_val[1] >= lo[1])) }

ltl correct_read_3 { []((writer@wf && reader[1]@rf && (lo[1] == hi[1])) -> (reader_val[1] == current_val)) }

